home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_b / c / spccluses3 < prev    next >
Text File  |  1996-08-28  |  1KB  |  62 lines
  1. typedef struct 
  2. {
  3.   int id;
  4.   char *name;
  5. } *record;
  6.  
  7. int *badResult (void)  
  8.   /* 1. Function result is used in defines clause of badResult but ...
  9.      2. Special clause accesses field of non-struct or union result */
  10.    /*@defines result->name@*/ 
  11. {
  12.   return NULL; /* 3. Null storage returned as non-null: NULL */
  13. } 
  14.  
  15. /*@special@*/ record createName (/*@only@*/ char *name)
  16.    /*@defines result->name@*/ 
  17. {
  18.   record res = (record) malloc (sizeof (*res));
  19.  
  20.   assert (res != NULL);
  21.   res->name = name;
  22.   return res;
  23. }
  24.  
  25. /*@special@*/ record createName2 (void)
  26.    /*@defines result->name@*/ 
  27. {
  28.   record res = (record) malloc (sizeof (*res));
  29.   return res; /* 4. Undefined storage res->name corresponds to storage listed ...
  30.          5. Possibly null storage res returned as non-null: res */
  31. }
  32.  
  33. /*@special@*/ record createName3 (void)
  34.    /*@defines result->id@*/ 
  35.    /*@allocates result->name@*/
  36. {
  37.   record res = (record) malloc (sizeof (*res));
  38.  
  39.   assert (res != NULL);
  40.  
  41.   res->name = (char *) malloc (sizeof (char) * 23);
  42.   res->id = 21;
  43.   return res;
  44. }
  45.  
  46. /*@special@*/ record createName4 (void)
  47.    /*@defines result->id@*/ 
  48.    /*@allocates result->name@*/
  49. {
  50.   record res = (record) malloc (sizeof (*res));
  51.  
  52.   assert (res != NULL);
  53.  
  54.   res->id = 21;
  55.   return res; /* 6. Unallocated storage res->name corresponds to storage ... */
  56. }
  57.  
  58.  
  59.  
  60.  
  61.  
  62.